g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
↳ QTRS
↳ DependencyPairsProof
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLD(t, x, s(n)) → F(fold(t, x, n), x)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
FOLD(t, x, s(n)) → FOLD(t, x, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLD(t, x, s(n)) → F(fold(t, x, n), x)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
FOLD(t, x, s(n)) → FOLD(t, x, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLDB(t, s(n)) → FOLDB(t, n)
Used ordering: Polynomial interpretation [25,35]:
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
The value of delta used in the strict ordering is 16.
POL(F''(x1)) = (4)x_1
POL(f''(x1)) = (4)x_1
POL(f(x1, x2)) = x_1
POL(g(x1)) = 0
POL(C) = 0
POL(FOLDC(x1, x2)) = (4)x_1
POL(A) = 0
POL(triple(x1, x2, x3)) = (4)x_2
POL(0) = 0
POL(f'(x1, x2)) = x_1
POL(foldC(x1, x2)) = x_1
POL(F'(x1, x2)) = (4)x_1
POL(B) = 4
POL(foldB(x1, x2)) = x_1
POL(s(x1)) = 4 + (4)x_1
POL(FOLDB(x1, x2)) = (4)x_1 + (4)x_2
POL(F(x1, x2)) = (4)x_1 + (4)x_2
foldB(t, 0) → t
foldC(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
f'(triple(a, b, c), C) → triple(a, b, s(c))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
FOLDC(t, s(n)) → FOLDC(t, n)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
Used ordering: Polynomial interpretation [25,35]:
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
The value of delta used in the strict ordering is 4.
POL(F''(x1)) = (4)x_1
POL(f''(x1)) = 2 + x_1
POL(f(x1, x2)) = 2 + x_1 + (4)x_2
POL(g(x1)) = 0
POL(C) = 0
POL(FOLDC(x1, x2)) = (4)x_1 + (4)x_2
POL(A) = 0
POL(triple(x1, x2, x3)) = (2)x_2 + x_3
POL(0) = 0
POL(f'(x1, x2)) = 2 + x_1
POL(foldC(x1, x2)) = 1 + x_1 + x_2
POL(F'(x1, x2)) = (4)x_1
POL(B) = 0
POL(foldB(x1, x2)) = x_1 + x_2
POL(s(x1)) = 2 + x_1
POL(FOLDB(x1, x2)) = (4)x_1 + (4)x_2
POL(F(x1, x2)) = (4)x_1
foldB(t, 0) → t
foldC(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
f'(triple(a, b, c), C) → triple(a, b, s(c))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(t, x) → F'(t, g(x))
Used ordering: Polynomial interpretation [25,35]:
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
The value of delta used in the strict ordering is 1.
POL(F'(x1, x2)) = x_2
POL(g(x1)) = (4)x_1
POL(B) = 1
POL(C) = 3
POL(A) = 0
POL(F(x1, x2)) = 1 + (4)x_2
POL(triple(x1, x2, x3)) = (3)x_1 + x_2
g(C) → B
g(C) → A
g(C) → C
g(A) → A
g(B) → A
g(B) → B
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
FOLD(t, x, s(n)) → FOLD(t, x, n)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLD(t, x, s(n)) → FOLD(t, x, n)
The value of delta used in the strict ordering is 4.
POL(FOLD(x1, x2, x3)) = (4)x_3
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)